$\forall$$A$:MsgA, $l$:IdLnk, $k$:Knd, $s$:$A$.state, $v$:$A$.da($k$).
\\[0ex]ma{-}frame{-}compat($A$;$A$)
\\[0ex]$\Rightarrow$ ($\neg$$A$.bframe($k$ sends on $l$))
\\[0ex]$\Rightarrow$ (filter($\lambda$${\it ms}$.mlnk(${\it ms}$) = $l$;$A$.sends($k$,$s$,$v$)) = [] $\in$ ($A$.Msg List))